Nuprl Lemma : no_repeats-before-equality 11,40

T:Type, as,bs:(T List).
no_repeats(Tas)
 no_repeats(Tbs)
 ((as = bs)
  ((x:T. (x  as (x  bs))
   (x,y:T. l_before(xyasT l_before(xybsT)))) 
latex


Definitionsx:AB(x), t  T, l_before(xylT), (x  l), Type, no_repeats(Tl), P  Q, x:AB(x), prop{i:l}, x:A  B(x), P  Q, P  Q, P  Q, type List, s = t, cons(carcdr), [], tl(l), n - m, if a<b then c else d, i <z j, b, i j, case b of inl(x) => s(x) | inr(y) => t(y), if b then t else f fi , nth_tl(n;as), hd(l), l[i], n + m, rec-case(a) of [] => s | x::y => z.t(x;y;z), x.A(x), Y, ||as||, a < b, A, A  B, , {x:AB(x)} , , False, guard(T), P  Q, left + right, xt(x), True, T
Lemmassquash wf, true wf, l before member2, l before member, no repeats cons, all functionality wrt iff, iff functionality wrt iff, cons before, cons member, nil member, iff wf, no repeats wf, l member wf, l before wf

origin